The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

append(@l1, @l2) → append#1(@l1, @l2)
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2))
append#1(nil, @l2) → @l2
appendAll(@l) → appendAll#1(@l)
appendAll#1(::(@l1, @ls)) → append(@l1, appendAll(@ls))
appendAll#1(nil) → nil
appendAll2(@l) → appendAll2#1(@l)
appendAll2#1(::(@l1, @ls)) → append(appendAll(@l1), appendAll2(@ls))
appendAll2#1(nil) → nil
appendAll3(@l) → appendAll3#1(@l)
appendAll3#1(::(@l1, @ls)) → append(appendAll2(@l1), appendAll3(@ls))
appendAll3#1(nil) → nil

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1)
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
append#1(nil, z0) → z0
appendAll(z0) → appendAll#1(z0)
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1))
appendAll#1(nil) → nil
appendAll2(z0) → appendAll2#1(z0)
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) → nil
appendAll3(z0) → appendAll3#1(z0)
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) → nil

Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPEND#1(nil, z0) → c2
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) → c5
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL2#1(nil) → c8
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
APPENDALL3#1(nil) → c11

S tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPEND#1(nil, z0) → c2
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) → c5
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL2#1(nil) → c8
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
APPENDALL3#1(nil) → c11

K tuples:none
Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 4 trailing nodes:

APPENDALL#1(nil) → c5
APPENDALL3#1(nil) → c11
APPEND#1(nil, z0) → c2
APPENDALL2#1(nil) → c8

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1)
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
append#1(nil, z0) → z0
appendAll(z0) → appendAll#1(z0)
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1))
appendAll#1(nil) → nil
appendAll2(z0) → appendAll2#1(z0)
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) → nil
appendAll3(z0) → appendAll3#1(z0)
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) → nil

Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

S tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

K tuples:none
Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

(5) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

We considered the (Usable) Rules:none
And the Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(::(x₁, x₂)) = [2] + x₁ + x₂   
POL(APPEND(x₁, x₂)) = 0   
POL(APPEND#1(x₁, x₂)) = 0   
POL(APPENDALL(x₁)) = 0   
POL(APPENDALL#1(x₁)) = 0   
POL(APPENDALL2(x₁)) = x₁   
POL(APPENDALL2#1(x₁)) = x₁   
POL(APPENDALL3(x₁)) = [1] + x₁   
POL(APPENDALL3#1(x₁)) = x₁   
POL(append(x₁, x₂)) = [1]   
POL(append#1(x₁, x₂)) = 0   
POL(appendAll(x₁)) = 0   
POL(appendAll#1(x₁)) = 0   
POL(appendAll2(x₁)) = [2] + [3]x₁   
POL(appendAll2#1(x₁)) = [1]   
POL(appendAll3(x₁)) = 0   
POL(appendAll3#1(x₁)) = 0   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c3(x₁)) = x₁   
POL(c4(x₁, x₂)) = x₁ + x₂   
POL(c6(x₁)) = x₁   
POL(c7(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c9(x₁)) = x₁   
POL(nil) = 0   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1)
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
append#1(nil, z0) → z0
appendAll(z0) → appendAll#1(z0)
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1))
appendAll#1(nil) → nil
appendAll2(z0) → appendAll2#1(z0)
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) → nil
appendAll3(z0) → appendAll3#1(z0)
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) → nil

Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

S tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))

K tuples:

APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

(7) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1)
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
append#1(nil, z0) → z0
appendAll(z0) → appendAll#1(z0)
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1))
appendAll#1(nil) → nil
appendAll2(z0) → appendAll2#1(z0)
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) → nil
appendAll3(z0) → appendAll3#1(z0)
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) → nil

Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

S tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))

K tuples:

APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))

Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))

We considered the (Usable) Rules:none
And the Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(::(x₁, x₂)) = [1] + x₁ + x₂   
POL(APPEND(x₁, x₂)) = 0   
POL(APPEND#1(x₁, x₂)) = 0   
POL(APPENDALL(x₁)) = x₁   
POL(APPENDALL#1(x₁)) = x₁   
POL(APPENDALL2(x₁)) = [1] + x₁   
POL(APPENDALL2#1(x₁)) = x₁   
POL(APPENDALL3(x₁)) = x₁   
POL(APPENDALL3#1(x₁)) = x₁   
POL(append(x₁, x₂)) = [1]   
POL(append#1(x₁, x₂)) = 0   
POL(appendAll(x₁)) = [1] + x₁   
POL(appendAll#1(x₁)) = [1]   
POL(appendAll2(x₁)) = 0   
POL(appendAll2#1(x₁)) = 0   
POL(appendAll3(x₁)) = [1] + x₁   
POL(appendAll3#1(x₁)) = [1] + x₁   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c3(x₁)) = x₁   
POL(c4(x₁, x₂)) = x₁ + x₂   
POL(c6(x₁)) = x₁   
POL(c7(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c9(x₁)) = x₁   
POL(nil) = [1]   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1)
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
append#1(nil, z0) → z0
appendAll(z0) → appendAll#1(z0)
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1))
appendAll#1(nil) → nil
appendAll2(z0) → appendAll2#1(z0)
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) → nil
appendAll3(z0) → appendAll3#1(z0)
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) → nil

Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

S tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))

K tuples:

APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))

Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

(11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1)
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
append#1(nil, z0) → z0
appendAll(z0) → appendAll#1(z0)
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1))
appendAll#1(nil) → nil
appendAll2(z0) → appendAll2#1(z0)
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) → nil
appendAll3(z0) → appendAll3#1(z0)
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) → nil

Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

S tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))

K tuples:

APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL(z0) → c3(APPENDALL#1(z0))

Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))

We considered the (Usable) Rules:

appendAll#1(::(z0, z1)) → append(z0, appendAll(z1))
append(z0, z1) → append#1(z0, z1)
append#1(nil, z0) → z0
appendAll(z0) → appendAll#1(z0)
appendAll2(z0) → appendAll2#1(z0)
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) → nil
appendAll#1(nil) → nil
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))

And the Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(::(x₁, x₂)) = [1] + x₁ + x₂   
POL(APPEND(x₁, x₂)) = x₁   
POL(APPEND#1(x₁, x₂)) = x₁   
POL(APPENDALL(x₁)) = x₁   
POL(APPENDALL#1(x₁)) = x₁   
POL(APPENDALL2(x₁)) = [2]x₁   
POL(APPENDALL2#1(x₁)) = [2]x₁   
POL(APPENDALL3(x₁)) = [2] + [3]x₁   
POL(APPENDALL3#1(x₁)) = [2] + [3]x₁   
POL(append(x₁, x₂)) = x₁ + x₂   
POL(append#1(x₁, x₂)) = x₁ + x₂   
POL(appendAll(x₁)) = x₁   
POL(appendAll#1(x₁)) = x₁   
POL(appendAll2(x₁)) = [3] + x₁   
POL(appendAll2#1(x₁)) = [3] + x₁   
POL(appendAll3(x₁)) = 0   
POL(appendAll3#1(x₁)) = 0   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c3(x₁)) = x₁   
POL(c4(x₁, x₂)) = x₁ + x₂   
POL(c6(x₁)) = x₁   
POL(c7(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c9(x₁)) = x₁   
POL(nil) = [2]   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1)
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
append#1(nil, z0) → z0
appendAll(z0) → appendAll#1(z0)
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1))
appendAll#1(nil) → nil
appendAll2(z0) → appendAll2#1(z0)
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) → nil
appendAll3(z0) → appendAll3#1(z0)
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) → nil

Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

S tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))

K tuples:

APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))

Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

(15) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))

Now S is empty

(16) BOUNDS(1, 1)